/* Copyright 2007 Nicola Olivetti, Gian Luca Pozzato This file is part of CondLean. CondLean is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version. CondLean is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with CondLean. If not, see . */ /* Theorem prover SeqCEM+CS+ID */ :- op(400,fy,neg), op(500,xfy,and), op(600,xfy,or), op(650,xfy,->), op(650,xfy,=>). :-use_module(library(lists)). /* --------------------------------------------------------------------------------------- */ /* The following predicate implements the calculi: prove(Cond,CEM,CS,ID,Sigma,Delta,Labels,ProofTree) :- Sigma |- Delta Cond is the list having elements [[x,a => b],[[x,a1,y1],[x,a2,y2],...,[x,an,yn]]]; each element represents that (=> L) has been applied (in that branch) by introducing the transition x-ai->yi in the left premise. CEM is as Cond in order to control the application of (CEM). It is a list of the form [[x,a,y],[[x,a1,y1],[x,a2,y2],...,[x,an,yn]]] CS is the list of transitions to which (CS) has already been applied in the current branch. In order to control the application of (CS), its application is restricted to transitions x-a->y such that x-a->y does not belong to the list CS ID is the list of transitions to which (ID) has already been applied in the current branch. In order to control the application of (ID), its application is restricted to transitions x-a->y such that x-a->y does not belong to the list ID Labels is the list of labels used in that branch; ProofTree is the proof tree built by the system and is used by the graphical interface written in Java */ /* Axioms */ /* true and false */ prove(_,_,_,_,[LitSigma,_,_],_,_,tree(falso)):- member([_,false],LitSigma),!. prove(_,_,_,_,_,[LitDelta,_,_],_,tree(vero)):- member([_,true],LitDelta),!. prove(_,_,_,_,[LitSigma,_,_],[LitDelta,_,_],_,tree(assioma)):- member(F,LitSigma),member(F,LitDelta),!. prove(_,_,_,_,[_,TransSigma,_],[_,TransDelta,_],_,tree(assioma)):- member(F,TransSigma),member(F,TransDelta),!. prove(_,_,_,_,[_,_,ComplexSigma],[_,_,ComplexDelta],_,tree(assioma)):- member(F,ComplexSigma),member(F,ComplexDelta),!. /* Rules */ /* and L */ prove(Cond,CEM,CS,ID,[LitSigma,TransSigma,ComplexSigma],Delta,Labels, tree(andL,ProofTail,[X,A and B])):- select([X,A and B],ComplexSigma,ResComplexSigma),!, put([X,A],LitSigma,ResComplexSigma,TempLitSigma,TempComplexSigma), put([X,B],TempLitSigma,TempComplexSigma,NewLitSigma,NewComplexSigma), prove(Cond,CEM,CS,ID,[NewLitSigma,TransSigma,NewComplexSigma],Delta,Labels,ProofTail). /* or R */ prove(Cond,CEM,CS,ID,Sigma,[LitDelta,TransDelta,ComplexDelta],Labels, tree(orR,ProofTail,[X,A or B])):- select([X,A or B],ComplexDelta,ResComplexDelta),!, put([X,A],LitDelta,ResComplexDelta,TempLitDelta,TempComplexDelta), put([X,B],TempLitDelta,TempComplexDelta,NewLitDelta,NewComplexDelta), prove(Cond,CEM,CS,ID,Sigma,[NewLitDelta,TransDelta,NewComplexDelta],Labels,ProofTail). /* neg R */ prove(Cond,CEM,CS,ID,[LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta], Labels,tree(negR,ProofTail,[X,neg A])):- select([X,neg A],ComplexDelta,ResComplexDelta),!, put([X,A],LitSigma,ComplexSigma,NewLitSigma,NewComplexSigma), prove(Cond,CEM,CS,ID,[NewLitSigma,TransSigma,NewComplexSigma],[LitDelta,TransDelta,ResComplexDelta], Labels,ProofTail). /* neg L */ prove(Cond,CEM,CS,ID,[LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta],Labels, tree(negL,ProofTail,[X,neg A])) :-select([X,neg A],ComplexSigma,ResComplexSigma),!, put([X,A],LitDelta,ComplexDelta,NewLitDelta,NewComplexDelta), prove(Cond,CEM,CS,ID,[LitSigma,TransSigma,ResComplexSigma],[NewLitDelta,TransDelta,NewComplexDelta], Labels,ProofTail). /* -> R */ prove(Cond,CEM,CS,ID,[LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta],Labels, tree(impR,ProofTail,[X,A -> B])) :-select([X,A -> B],ComplexDelta,ResComplexDelta),!, put([X,A],LitSigma,ComplexSigma,NewLitSigma,NewComplexSigma), put([X,B],LitDelta,ResComplexDelta,NewLitDelta,NewComplexDelta), prove(Cond,CEM,CS,ID,[NewLitSigma,TransSigma,NewComplexSigma],[NewLitDelta,TransDelta,NewComplexDelta], Labels,ProofTail). /* => R */ prove(Cond,CEM,CS,ID,[LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta],Labels, tree(condR,ProofTail,Y,[X,A => B])) :-select([X,A => B],ComplexDelta,ResComplexDelta),!, generaLabels(Y,Labels), put([Y,B],LitDelta,ResComplexDelta,NewLitDelta,NewComplexDelta), prove(Cond,CEM,CS,ID,[LitSigma,[[X,A,Y]|TransSigma],ComplexSigma],[NewLitDelta,TransDelta,NewComplexDelta], [Y|Labels],ProofTail). /* ID */ prove(Cond,CEM,CS,ID,[LitSigma,TransSigma,ComplexSigma],Delta,Labels,tree(id,ProofTail,[X,A,Y])):- member([X,A,Y],TransSigma), \+member([X,A,Y],ID),!, put([Y,A],LitSigma,ComplexSigma,NewLitSigma,NewComplexSigma), prove(Cond,CEM,CS,[[X,A,Y]|ID],[NewLitSigma,TransSigma,NewComplexSigma],Delta,Labels,ProofTail). /* and R */ prove(Cond,CEM,CS,ID,Sigma,[LitDelta,TransDelta,ComplexDelta],Labels, tree(andR,LeftProof,RightProof,[X,A and B])):- select([X,A and B],ComplexDelta,ResComplexDelta),!, put([X,A],LitDelta,ResComplexDelta,FirstLitDelta,FirstComplexDelta), put([X,B],LitDelta,ResComplexDelta,SecLitDelta,SecComplexDelta), prove(Cond,CEM,CS,ID,Sigma,[FirstLitDelta,TransDelta,FirstComplexDelta],Labels,LeftProof), prove(Cond,CEM,CS,ID,Sigma,[SecLitDelta,TransDelta,SecComplexDelta],Labels,RightProof). /* or L */ prove(Cond,CEM,CS,ID,[LitSigma,TransSigma,ComplexSigma],Delta,Labels, tree(orL,LeftProof,RightProof,[X,A or B])):- select([X,A or B],ComplexSigma,ResComplexSigma),!, put([X,A],LitSigma,ResComplexSigma,FirstLitSigma,FirstComplexSigma), put([X,B],LitSigma,ResComplexSigma,SecLitSigma,SecComplexSigma), prove(Cond,CEM,CS,ID,[FirstLitSigma,TransSigma,FirstComplexSigma],Delta,Labels,LeftProof), prove(Cond,CEM,CS,ID,[SecLitSigma,TransSigma,SecComplexSigma],Delta,Labels,RightProof). /* -> L */ prove(Cond,CEM,CS,ID,[LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta],Labels, tree(impL,LeftTail,RightTail,[X,A -> B])):- select([X,A -> B],ComplexSigma,ResComplexSigma),!, put([X,A],LitDelta,ComplexDelta,NewLitDelta,NewComplexDelta), put([X,B],LitSigma,ResComplexSigma,NewLitSigma,NewComplexSigma), prove(Cond,CEM,CS,ID,[LitSigma,TransSigma,ResComplexSigma],[NewLitDelta,TransDelta,NewComplexDelta], Labels,LeftTail), prove(Cond,CEM,CS,ID,[NewLitSigma,TransSigma,NewComplexSigma],[LitDelta,TransDelta,ComplexDelta], Labels,RightTail). /* CS */ prove(Cond,CEM,CS,ID,[LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta],Labels, tree(cs,LeftProof,RightProof,U,[X,A,Y])):- member([X,A,Y],TransSigma), X\=Y, \+member([X,A,Y],CS),!, put([X,A],LitDelta,ComplexDelta,NewLitDelta,NewComplexDelta), prove(Cond,CEM,[[X,A,Y]|CS],ID,[LitSigma,TransSigma,ComplexSigma],[NewLitDelta,TransDelta,NewComplexDelta],Labels,LeftProof), generaLabels(U,Labels), labelSubstitution(LitSigma,X,U,TempLitSigma), labelSubstitution(TempLitSigma,Y,U,DefLitSigma), labelSubstitution(TransSigma,X,U,TempTransSigma), labelSubstitution(TempTransSigma,Y,U,DefTransSigma), labelSubstitution(ComplexSigma,X,U,TempComplexSigma), labelSubstitution(TempComplexSigma,Y,U,DefComplexSigma), labelSubstitution(LitDelta,X,U,TempLitDelta), labelSubstitution(TempLitDelta,Y,U,DefLitDelta), labelSubstitution(TransDelta,X,U,TempTransDelta), labelSubstitution(TempTransDelta,Y,U,DefTransDelta), labelSubstitution(ComplexDelta,X,U,TempComplexDelta), labelSubstitution(TempComplexDelta,Y,U,DefComplexDelta), prove(Cond,CEM,CS,ID,[DefLitSigma,DefTransSigma,DefComplexSigma], [DefLitDelta,DefTransDelta,DefComplexDelta],[U|Labels],RightProof). /* => L */ /* This rule is invertible (thus the cut) and needs to be applied only by using transitions X-A->Y such that X-C->Y belongs to the left-hand side of the sequent */ /* In this first clause, (=> L) has never been applied to that principal formula, yet */ prove(Cond,CEM,CS,ID,[LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta],Labels, tree(condL,LeftTail,RightTail,Y,[X,A => B])):- member([X,A => B],ComplexSigma), \+member([[X,A => B],_],Cond), member([X,C,Y],TransSigma),!, prove([[[X,A=>B],[[X,C,Y]]]|Cond],CEM,CS,ID,[LitSigma,TransSigma,ComplexSigma],[LitDelta,[[X,A,Y]|TransDelta],ComplexDelta], Labels,LeftTail), put([Y,B],LitSigma,ComplexSigma,ResLitSigma,ResComplexSigma), prove([[[X,A=>B],[[X,C,Y]]]|Cond],CEM,CS,ID,[ResLitSigma,TransSigma,ResComplexSigma],[LitDelta,TransDelta,ComplexDelta], Labels,RightTail). /* => L */ /* In this second clause, (=> L) is applied by choosing an "available" label, excluding those contained in the corresponding item in the list Cond */ prove(Cond,CEM,CS,ID,[LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta],Labels, tree(condL,LeftTail,RightTail,Y,[X,A => B])):- member([X,A => B],ComplexSigma), select([[X,A => B],Used],Cond,TempCond), member([X,C,Y],TransSigma), \+member([X,C,Y],Used),!, prove([[[X,A => B],[[X,C,Y]|Used]]|TempCond],CEM,CS,ID,[LitSigma,TransSigma,ComplexSigma], [LitDelta,[[X,A,Y]|TransDelta],ComplexDelta],Labels,LeftTail), put([Y,B],LitSigma,ComplexSigma,ResLitSigma,ResComplexSigma), prove([[[X,A => B],[[X,C,Y]|Used]]|TempCond],CEM,CS,ID,[ResLitSigma,TransSigma,ResComplexSigma], [LitDelta,TransDelta,ComplexDelta],Labels,RightTail). /* CEM */ /* As for (=>L), we have several caluses: each one of them consider a possibile case */ prove(Cond,CEM,CS,ID,[LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta],Labels, tree(cem,LeftProof,RightProof,U,Z,[X,A,Y])):- member([X,A,Y],TransSigma), /* (CEM) has never been applied to X-A->Y, yet */ \+member([[X,A,Y],_],CEM), member([X,B,Z],TransSigma), Y\=Z,!, prove(Cond,[[[X,A,Y],[[X,B,Z]]]|CEM],CS,ID,[LitSigma,TransSigma,ComplexSigma],[LitDelta,[[X,A,Z]|TransDelta],ComplexDelta],Labels,LeftProof), generaLabels(U,Labels), labelSubstitution(LitSigma,Z,U,TempLitSigma), labelSubstitution(TempLitSigma,Y,U,DefLitSigma), labelSubstitution(TransSigma,Z,U,TempTransSigma), labelSubstitution(TempTransSigma,Y,U,DefTransSigma), labelSubstitution(ComplexSigma,Z,U,TempComplexSigma), labelSubstitution(TempComplexSigma,Y,U,DefComplexSigma), labelSubstitution(LitDelta,Z,U,TempLitDelta), labelSubstitution(TempLitDelta,Y,U,DefLitDelta), labelSubstitution(TransDelta,Z,U,TempTransDelta), labelSubstitution(TempTransDelta,Y,U,DefTransDelta), labelSubstitution(ComplexDelta,Z,U,TempComplexDelta), labelSubstitution(TempComplexDelta,Y,U,DefComplexDelta), prove(Cond,[[[X,A,Y],[[X,B,Z]]]|CEM],CS,ID,[DefLitSigma,DefTransSigma,DefComplexSigma],[DefLitDelta,DefTransDelta,DefComplexDelta],[U|Labels],RightProof). prove(Cond,CEM,CS,ID,[LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta],Labels, tree(cem,LeftProof,RightProof,U,Z,[X,A,Y])):- member([X,A,Y],TransSigma), /* (CEM) has already been applied to X-A->Y */ select([[X,A,Y],Used],CEM,NewCEM), member([X,B,Z],TransSigma), Y\=Z, \+member([X,B,Z],Used), !, prove(Cond,[[[X,A,Y],[[X,B,Z]|Used]]|NewCEM],CS,ID,[LitSigma,TransSigma,ComplexSigma],[LitDelta,[[X,A,Z]|TransDelta],ComplexDelta],Labels,LeftProof), generaLabels(U,Labels), labelSubstitution(LitSigma,Z,U,TempLitSigma), labelSubstitution(TempLitSigma,Y,U,DefLitSigma), labelSubstitution(TransSigma,Z,U,TempTransSigma), labelSubstitution(TempTransSigma,Y,U,DefTransSigma), labelSubstitution(ComplexSigma,Z,U,TempComplexSigma), labelSubstitution(TempComplexSigma,Y,U,DefComplexSigma), labelSubstitution(LitDelta,Z,U,TempLitDelta), labelSubstitution(TempLitDelta,Y,U,DefLitDelta), labelSubstitution(TransDelta,Z,U,TempTransDelta), labelSubstitution(TempTransDelta,Y,U,DefTransDelta), labelSubstitution(ComplexDelta,Z,U,TempComplexDelta), labelSubstitution(TempComplexDelta,Y,U,DefComplexDelta), prove(Cond,[[[X,A,Y],[[X,B,Z]|Used]]|NewCEM],CS,ID,[DefLitSigma,DefTransSigma,DefComplexSigma],[DefLitDelta,DefTransDelta,DefComplexDelta],[U|Labels],RightProof). /* EQ */ prove(_,_,_,_,[_,TransSigma,_],[_,TransDelta,_],_,tree(eq,LeftProof,RightProof,[X,A,Y],[X,B,Y])):- member([X,A,Y],TransSigma),member([X,B,Y],TransDelta), /* The premises are "independent" from the conclusion, so we can use label x for their proofs */ put([x,A],[],[],FirstLitSigma,FirstComplexSigma), put([x,B],[],[],FirstLitDelta,FirstComplexDelta), put([x,B],[],[],SecLitSigma,SecComplexSigma), put([x,A],[],[],SecLitDelta,SecComplexDelta), prove([],[],[],[],[FirstLitSigma,[],FirstComplexSigma],[FirstLitDelta,[],FirstComplexDelta], [x],LeftProof), prove([],[],[],[],[SecLitSigma,[],SecComplexSigma],[SecLitDelta,[],SecComplexDelta], [x],RightProof). /* --------------------------------------------------------------------------------------- */ /* Auxiliary predicates for the (CS) rule */ labelSubstitution([],_,_,[]):-!. labelSubstitution([[X,F]|Tail],X,U,[[U,F]|ResTail]):-labelSubstitution(Tail,X,U,ResTail). labelSubstitution([[X,F,X]|Tail],X,U,[[U,F,U]|ResTail]):-labelSubstitution(Tail,X,U,ResTail). labelSubstitution([[X,F,Y]|Tail],X,U,[[U,F,Y]|ResTail]):-X\=Y,labelSubstitution(Tail,X,U,ResTail). labelSubstitution([[Y,F,X]|Tail],X,U,[[Y,F,U]|ResTail]):-X\=Y,labelSubstitution(Tail,X,U,ResTail). labelSubstitution([[Y,F,Z]|Tail],X,U,[[Y,F,Z]|ResTail]):-X\=Y,X\=Z,labelSubstitution(Tail,X,U,ResTail). labelSubstitution([[Y,F]|Tail],X,U,[[Y,F]|ResTail]):-Y\=X,labelSubstitution(Tail,X,U,ResTail). /* --------------------------------------------------------------------------------------- */ /* This predicate generates a "new" label for that branch */ generaLabels(x,Labels):-true,\+member(x,Labels),!. generaLabels(y,Labels):-true,\+member(y,Labels),!. generaLabels(z,Labels):-true,\+member(z,Labels),!. generaLabels(u,Labels):-true,\+member(z,Labels),!. generaLabels(v,Labels):-true,\+member(z,Labels),!. generaLabels(w,Labels):-true,\+member(z,Labels),!. generaLabels(k,Labels):-true,\+member(k,Labels),!. generaLabels(j,Labels):-true,\+member(j,Labels),!. generaLabels(i,Labels):-true,\+member(i,Labels),!. generaLabels(x+1,[i|_]):-!. generaLabels(x+N1,[Last|_]):-Last=x+N,N1 is N+1,!. /* This predicate finds all the labels in the sequent etichette(+Sequente,-ListaEtichette) */ etichette([],[]):-!. etichette([[L,_]|Tail],[L|TailLab]):-etichette(Tail,TailLab),\+member(L,TailLab),!. etichette([[L,_,L]|Tail],[L|TailLab]):-etichette(Tail,TailLab),\+member(L,TailLab),!. etichette([[L1,_,L2]|Tail],[L1,L2|TailLab]):-etichette(Tail,TailLab), \+member(L1,TailLab),\+member(L2,TailLab),!. etichette([[L1,_,L2]|Tail],[L1|TailLab]):-etichette(Tail,TailLab), \+member(L1,TailLab),member(L2,TailLab),!. etichette([[L1,_,L2]|Tail],[L2|TailLab]):-etichette(Tail,TailLab), \+member(L2,TailLab),member(L1,TailLab),!. etichette([_|Tail],Labels):-etichette(Tail,Labels). /* This predicate creates a partition of the sequent in atomic, transition and complex formulas */ struttura([],[],[],[]):-!. struttura([[X,A and B]|Tail],Literal,Transaction,[[X,A and B]|ForTail]):- struttura(Tail,Literal,Transaction,ForTail),!. struttura([[X,A or B]|Tail],Literal,Transaction,[[X,A or B]|ForTail]):- struttura(Tail,Literal,Transaction,ForTail),!. struttura([[X,A -> B]|Tail],Literal,Transaction,[[X,A -> B]|ForTail]):- struttura(Tail,Literal,Transaction,ForTail),!. struttura([[X,A => B]|Tail],Literal,Transaction,[[X,A => B]|ForTail]):- struttura(Tail,Literal,Transaction,ForTail),!. struttura([[X,neg A]|Tail],Literal,Transaction,[[X,neg A]|ForTail]):- struttura(Tail,Literal,Transaction,ForTail),!. struttura([[X,A,Y]|Tail],Literal,[[X,A,Y]|TransTail],Formulae):- struttura(Tail,Literal,TransTail,Formulae),!. struttura([X|Tail],[X|LitTail],Transition,Formulae):- struttura(Tail,LitTail,Transition,Formulae),!. /* This predicate inserts a formula in the correct list; more precisely, a formula can be an atomic formula or a complex formula */ put([X,A and B],Literal,Formulae,Literal,[[X,A and B]|Formulae]):-!. put([X,A or B],Literal,Formulae,Literal,[[X,A or B]|Formulae]):-!. put([X,A -> B],Literal,Formulae,Literal,[[X,A -> B]|Formulae]):-!. put([X,A => B],Literal,Formulae,Literal,[[X,A => B]|Formulae]):-!. put([X,neg A],Literal,Formulae,Literal,[[X,neg A]|Formulae]):-!. put(X,Literal,Formulae,[X|Literal],Formulae):-!. /* --------------------------------------------------------------------------------------- */ /* All the following predicates are used to link the SICStus Prolog implementation to the graphical interface */ /* --------------------------------------------------------------------------------------- */ /* This predicate is invoked from the graphical interface (Java) */ proof(Sigma,Delta,JavaProof,LunghSeq,GradoSeq,NumEtichette,Altezza,NumNodi, NumCondR,NumCondL,NumEq,NumContr):- append(Sigma,Delta,T),etichette(T,Labels), struttura(Sigma,LitSigma,TransSigma,ForSigma), struttura(Delta,LitDelta,TransDelta,ForDelta), prove([],[],[],[],[LitSigma,TransSigma,ForSigma],[LitDelta,TransDelta,ForDelta],Labels,ProofTree), costruisciJava(ProofTree,[[LitSigma,TransSigma,ForSigma],[LitDelta,TransDelta,ForDelta]], JavaProof), lunghezzaSequente(Sigma,LSigma),lunghezzaSequente(Delta,LDelta),LunghSeq is LSigma+LDelta, gradoSequente(ForSigma,GSigma),gradoSequente(ForDelta,GDelta),GradoSeq is GSigma+GDelta, etichetteUsate(JavaProof,NumEtichette), altezzaAlbero(JavaProof,Altezza), nodiAlbero(JavaProof,NumNodi), condADestra(JavaProof,NumCondR), condASinistra(JavaProof,NumCondL), eqPresenti(JavaProof,NumEq), contrazioni(JavaProof,NumContr). /* --------------------------------------------------------------------------------------- */ /* Statistics */ contrazioni(_,0). eqPresenti(null,0). eqPresenti(new_Tree(_,eq,_,_,_,LeftProof,RightProof),NumEq):-!, eqPresenti(LeftProof,EqL),eqPresenti(RightProof,EqR),NumEq is 1+EqL+EqR. eqPresenti(new_Tree(_,_,_,_,_,LeftProof,RightProof),NumEq):- eqPresenti(LeftProof,EqL),eqPresenti(RightProof,EqR),NumEq is EqL+EqR. condADestra(null,0). condADestra(new_Tree(_,condR,_,_,_,LeftProof,RightProof),NumCondR):-!, condADestra(LeftProof,CondL),condADestra(RightProof,CondR), NumCondR is 1+CondL+CondR. condADestra(new_Tree(_,_,_,_,_,LeftProof,RightProof),NumCondR):- condADestra(LeftProof,CondL),condADestra(RightProof,CondR), NumCondR is CondL+CondR. condASinistra(null,0). condASinistra(new_Tree(_,condL,_,_,_,LeftProof,RightProof),NumCondL):-!, condASinistra(LeftProof,CondL),condASinistra(RightProof,CondR), NumCondL is 1+CondL+CondR. condASinistra(new_Tree(_,_,_,_,_,LeftProof,RightProof),NumCondL):- condASinistra(LeftProof,CondL),condASinistra(RightProof,CondR), NumCondL is CondL+CondR. nodiAlbero(null,0). nodiAlbero(new_Tree(_,_,_,_,_,LeftProof,RightProof),Nodi):-nodiAlbero(LeftProof,NodiL), nodiAlbero(RightProof,NodiR),Nodi is 1+NodiL+NodiR. altezzaAlbero(null,0). altezzaAlbero(new_Tree(_,_,_,_,_,LeftProof,RightProof),Heigth):- altezzaAlbero(LeftProof,Left),altezzaAlbero(RightProof,Right), massimo(Left,Right,Max),Heigth is 1+Max. massimo(A,B,A):-A>B,!. massimo(_,B,B). etichetteUsate(JavaProof,NumEtichette):-elencoLabels(JavaProof,ListaLabels), remove_duplicates(ListaLabels,ListaFinale),length(ListaFinale,NumEtichette). elencoLabels(null,[]). elencoLabels(new_Tree(Sequente,_,_,_,_,LeftProof,RightProof),ListaEtichette):- elencoLabSequente(Sequente,ListaSeq),elencoLabels(LeftProof,LeftLab), elencoLabels(RightProof,RightLab),append(ListaSeq,LeftLab,Temp), append(Temp,RightLab,ListaEtichette). elencoLabSequente([],[]). elencoLabSequente([[X,_]|Tail],[X|TailLab]):-elencoLabSequente(Tail,TailLab). elencoLabSequente([[X,_,Y]|Tail],[X,Y|TailLab]):-elencoLabSequente(Tail,TailLab). elencoLabSequente([*|Tail],TailLab):-elencoLabSequente(Tail,TailLab). lunghezzaSequente([],0). lunghezzaSequente([[_,A]|Tail],Lung):-complessita(A,Compl), lunghezzaSequente(Tail,LungTail),Lung is 2*Compl+LungTail. lunghezzaSequente([[_,A,_]|Tail],Lung):-complessita(A,Compl), lunghezzaSequente(Tail,LungTail),Lung is 1+2*Compl+LungTail. complessita(neg A,Compl):-complessita(A,ComplResto),Compl is 1+ComplResto. complessita(A and B,Compl):-complessita(A,ComplA),complessita(B,ComplB), Compl is 1+ComplA+ComplB. complessita(A or B,Compl):-complessita(A,ComplA),complessita(B,ComplB), Compl is 1+ComplA+ComplB. complessita(A -> B,Compl):-complessita(A,ComplA),complessita(B,ComplB), Compl is 1+ComplA+ComplB. complessita(A => B,Compl):-complessita(A,ComplA),complessita(B,ComplB), Compl is 1+ComplA+ComplB. complessita(_,1). gradoSequente([],0). gradoSequente([[_,A]|Tail],Grado):-grado(A,GrA), gradoSequente(Tail,GradoTail),massimo(GrA,GradoTail,Grado). gradoSequente([[_,A,_]|Tail],Grado):-grado(A,GrA), gradoSequente(Tail,GradoTail),massimo(GrA,GradoTail,Grado). grado(neg A,GrA):-grado(A,GrA). grado(A and B,Grado):-grado(A,GrA),grado(B,GrB),massimo(GrA,GrB,Grado). grado(A or B,Grado):-grado(A,GrA),grado(B,GrB),massimo(GrA,GrB,Grado). grado(A -> B,Grado):-grado(A,GrA),grado(B,GrB),massimo(GrA,GrB,Grado). grado(A => B,Grado):-grado(A,GrA),grado(B,GrB),massimo(GrA,GrB,Max),Grado is Max+1. grado(_,0). sequente(new_Tree(Sequente,_,_,_,_,_,_),Sequente). regola(new_Tree(_,Rule,_,_,_,_,_),Rule). antecedenteFormulaPrincipale(new_Tree(_,_,[Antec,_],_,_,_,_),Antec). conseguenteFormulaPrincipale(new_Tree(_,_,[_,Conseg],_,_,_,_),Conseg). antecedentePremessaSinistra(new_Tree(_,_,_,[Antec,_],_,_,_),Antec). conseguentePremessaSinistra(new_Tree(_,_,_,[_,Conseg],_,_,_),Conseg). antecedentePremessaDestra(new_Tree(_,_,_,_,[Antec,_],_,_),Antec). conseguentePremessaDestra(new_Tree(_,_,_,_,[_,Conseg],_,_),Conseg). alberoSinistro(new_Tree(_,_,_,_,_,Sinistro,_),Sinistro). alberoDestro(new_Tree(_,_,_,_,_,_,Destro),Destro). /* --------------------------------------------------------------------------------------- */ /* This predicate "destroies" the partition in a sequent */ appiattisci([Lit,Trans,Lab],Result):-append(Lit,Trans,Temp), append(Temp,Lab,Result). /* This predicate builds a proof tree used by the graphical interface */ /* Axioms */ costruisciJava(tree(falso),[Sigma,Delta], new_Tree(Sequente,assioma,[[X,false],[]],[[],[]],[[],[]],null,null)):- appiattisci(Sigma,Antecedente), appiattisci(Delta,Conseguente), member([X,false],Antecedente), append(Antecedente,[*],Temp), append(Temp,Conseguente,Sequente). costruisciJava(tree(vero),[Sigma,Delta], new_Tree(Sequente,assioma,[[],[X,true]],[[],[]],[[],[]],null,null)):- appiattisci(Sigma,Antecedente), appiattisci(Delta,Conseguente), member([X,true],Conseguente), append(Antecedente,[*],Temp), append(Temp,Conseguente,Sequente). costruisciJava(tree(assioma),[Sigma,Delta], new_Tree(Sequente,assioma,[[F],[F]],[[],[]],[[],[]],null,null)):- appiattisci(Sigma,Antecedente), appiattisci(Delta,Conseguente), member(F,Antecedente),member(F,Conseguente), append(Antecedente,[*],Temp), append(Temp,Conseguente,Sequente). /* Rules */ /* and L */ costruisciJava(tree(andL,LeftProof,[X,A and B]), [[LitSigma,TransSigma,ComplexSigma],Delta], new_Tree(Sequente,andL,[[[X,A and B]],[]],[[[X,A],[X,B]],[]],[[],[]],JavaLeft,null)):- appiattisci([LitSigma,TransSigma,ComplexSigma],Antecedente), appiattisci(Delta,Conseguente), append(Antecedente,[*],Temp), append(Temp,Conseguente,Sequente), delete(ComplexSigma,[X,A and B],ResComplexSigma), put([X,A],LitSigma,ResComplexSigma,TempLitSigma,TempComplexSigma), put([X,B],TempLitSigma,TempComplexSigma,NewLitSigma,NewComplexSigma), costruisciJava(LeftProof,[[NewLitSigma,TransSigma,NewComplexSigma],Delta],JavaLeft). /* or R */ costruisciJava(tree(orR,LeftProof,[X,A or B]), [Sigma,[LitDelta,TransDelta,ComplexDelta]], new_Tree(Sequente,orR,[[],[[X,A or B]]],[[],[[X,A],[X,B]]],[[],[]],JavaLeft,null)):- appiattisci(Sigma,Antecedente), appiattisci([LitDelta,TransDelta,ComplexDelta],Conseguente), append(Antecedente,[*],Temp), append(Temp,Conseguente,Sequente), delete(ComplexDelta,[X,A or B],ResComplexDelta), put([X,A],LitDelta,ResComplexDelta,TempLitDelta,TempComplexDelta), put([X,B],TempLitDelta,TempComplexDelta,NewLitDelta,NewComplexDelta), costruisciJava(LeftProof,[Sigma,[NewLitDelta,TransDelta,NewComplexDelta]],JavaLeft). /* neg R */ costruisciJava(tree(negR,LeftProof,[X,neg A]), [[LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta]], new_Tree(Sequente,negR,[[],[[X,neg A]]],[[[X,A]],[]],[[],[]],JavaLeft,null)):- appiattisci([LitSigma,TransSigma,ComplexSigma],Antecedente), appiattisci([LitDelta,TransDelta,ComplexDelta],Conseguente), append(Antecedente,[*],Temp), append(Temp,Conseguente,Sequente), delete(ComplexDelta,[X,neg A],ResComplexDelta), put([X,A],LitSigma,ComplexSigma,NewLitSigma,NewComplexSigma), costruisciJava(LeftProof,[[NewLitSigma,TransSigma,NewComplexSigma], [LitDelta,TransDelta,ResComplexDelta]],JavaLeft). /* neg L */ costruisciJava(tree(negL,LeftProof,[X,neg A]), [[LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta]], new_Tree(Sequente,negL,[[[X,neg A]],[]],[[],[[X,A]]],[[],[]],JavaLeft,null)):- appiattisci([LitSigma,TransSigma,ComplexSigma],Antecedente), appiattisci([LitDelta,TransDelta,ComplexDelta],Conseguente), append(Antecedente,[*],Temp), append(Temp,Conseguente,Sequente), delete(ComplexSigma,[X,neg A],ResComplexSigma), put([X,A],LitDelta,ComplexDelta,NewLitDelta,NewComplexDelta), costruisciJava(LeftProof,[[LitSigma,TransSigma,ResComplexSigma], [NewLitDelta,TransDelta,NewComplexDelta]],JavaLeft). /* -> R */ costruisciJava(tree(impR,LeftProof,[X,A -> B]), [[LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta]], new_Tree(Sequente,impR,[[],[[X,A -> B]]],[[[X,A]],[[X,B]]],[[],[]],JavaLeft,null)):- appiattisci([LitSigma,TransSigma,ComplexSigma],Antecedente), appiattisci([LitDelta,TransDelta,ComplexDelta],Conseguente), append(Antecedente,[*],Temp), append(Temp,Conseguente,Sequente), delete(ComplexDelta,[X,A -> B],ResComplexDelta), put([X,A],LitSigma,ComplexSigma,NewLitSigma,NewComplexSigma), put([X,B],LitDelta,ResComplexDelta,NewLitDelta,NewComplexDelta), costruisciJava(LeftProof,[[NewLitSigma,TransSigma,NewComplexSigma], [NewLitDelta,TransDelta,NewComplexDelta]],JavaLeft). /* => R */ costruisciJava(tree(condR,LeftProof,Y,[X,A => B]), [[LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta]], new_Tree(Sequente,condR,[[],[[X,A => B]]],[[[X,A,Y]],[[Y,B]]],[[],[]],JavaLeft,null)):- appiattisci([LitSigma,TransSigma,ComplexSigma],Antecedente), appiattisci([LitDelta,TransDelta,ComplexDelta],Conseguente), append(Antecedente,[*],Temp), append(Temp,Conseguente,Sequente), delete(ComplexDelta,[X,A => B],ResComplexDelta), put([Y,B],LitDelta,ResComplexDelta,NewLitDelta,NewComplexDelta), costruisciJava(LeftProof,[[LitSigma,[[X,A,Y]|TransSigma],ComplexSigma], [NewLitDelta,TransDelta,NewComplexDelta]],JavaLeft). /* and R */ costruisciJava(tree(andR,LeftProof,RightProof,[X,A and B]), [Sigma,[LitDelta,TransDelta,ComplexDelta]], new_Tree(Sequente,andR,[[],[[X,A and B]]],[[],[[X,A]]],[[],[[X,B]]],JavaLeft,JavaRight)):- appiattisci(Sigma,Antecedente), appiattisci([LitDelta,TransDelta,ComplexDelta],Conseguente), append(Antecedente,[*],Temp), append(Temp,Conseguente,Sequente), delete(ComplexDelta,[X,A and B],ResComplexDelta), put([X,A],LitDelta,ResComplexDelta,FirstLitDelta,FirstComplexDelta), put([X,B],LitDelta,ResComplexDelta,SecLitDelta,SecComplexDelta), costruisciJava(LeftProof,[Sigma,[FirstLitDelta,TransDelta,FirstComplexDelta]],JavaLeft), costruisciJava(RightProof,[Sigma,[SecLitDelta,TransDelta,SecComplexDelta]],JavaRight). /* or L */ costruisciJava(tree(orL,LeftProof,RightProof,[X,A or B]), [[LitSigma,TransSigma,ComplexSigma],Delta], new_Tree(Sequente,orL,[[[X,A or B]],[]],[[[X,A]],[]],[[[X,B]],[]],JavaLeft,JavaRight)):- appiattisci([LitSigma,TransSigma,ComplexSigma],Antecedente), appiattisci(Delta,Conseguente), append(Antecedente,[*],Temp), append(Temp,Conseguente,Sequente), delete(ComplexSigma,[X,A or B],ResComplexSigma), put([X,A],LitSigma,ResComplexSigma,FirstLitSigma,FirstComplexSigma), put([X,B],LitSigma,ResComplexSigma,SecLitSigma,SecComplexSigma), costruisciJava(LeftProof,[[FirstLitSigma,TransSigma,FirstComplexSigma],Delta],JavaLeft), costruisciJava(RightProof,[[SecLitSigma,TransSigma,SecComplexSigma],Delta],JavaRight). /* -> L */ costruisciJava(tree(impL,LeftProof,RightProof,[X,A -> B]), [[LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta]], new_Tree(Sequente,impL,[[[X,A -> B]],[]],[[],[[X,A]]],[[[X,B]],[]],JavaLeft,JavaRight)):- appiattisci([LitSigma,TransSigma,ComplexSigma],Antecedente), appiattisci([LitDelta,TransDelta,ComplexDelta],Conseguente), append(Antecedente,[*],Temp), append(Temp,Conseguente,Sequente), delete(ComplexSigma,[X,A -> B],ResComplexSigma), put([X,A],LitDelta,ComplexDelta,NewLitDelta,NewComplexDelta), put([X,B],LitSigma,ResComplexSigma,NewLitSigma,NewComplexSigma), costruisciJava(LeftProof,[[LitSigma,TransSigma,ResComplexSigma], [NewLitDelta,TransDelta,NewComplexDelta]],JavaLeft), costruisciJava(RightProof,[[NewLitSigma,TransSigma,NewComplexSigma], [LitDelta,TransDelta,ComplexDelta]],JavaRight). /* => L */ costruisciJava(tree(condL,LeftProof,RightProof,Y,[X,A => B]), [[LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta]], new_Tree(Sequente,condL,[[[X,A => B]],[]],[[],[[X,A,Y]]],[[[Y,B]],[]],JavaLeft,JavaRight)):- appiattisci([LitSigma,TransSigma,ComplexSigma],Antecedente), appiattisci([LitDelta,TransDelta,ComplexDelta],Conseguente), append(Antecedente,[*],Temp), append(Temp,Conseguente,Sequente), put([Y,B],LitSigma,ComplexSigma,NewLitSigma,NewComplexSigma), costruisciJava(LeftProof,[[LitSigma,TransSigma,ComplexSigma], [LitDelta,[[X,A,Y]|TransDelta],ComplexDelta]],JavaLeft), costruisciJava(RightProof,[[NewLitSigma,TransSigma,NewComplexSigma], [LitDelta,TransDelta,ComplexDelta]],JavaRight). /* EQ */ costruisciJava(tree(eq,LeftProof,RightProof,[X,A,Y],[X,B,Y]), [[LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta]], new_Tree(Sequente,eq,[[[X,A,Y]],[[X,B,Y]]],[[[x,A]],[[x,B]]], [[[x,B]],[[x,A]]],JavaLeft,JavaRight)):- appiattisci([LitSigma,TransSigma,ComplexSigma],Antecedente), appiattisci([LitDelta,TransDelta,ComplexDelta],Conseguente), append(Antecedente,[*],Temp), append(Temp,Conseguente,Sequente), put([x,A],[],[],FirstLitSigma,FirstComplexSigma), put([x,B],[],[],FirstLitDelta,FirstComplexDelta), put([x,B],[],[],SecLitSigma,SecComplexSigma), put([x,A],[],[],SecLitDelta,SecComplexDelta), costruisciJava(LeftProof,[[FirstLitSigma,[],FirstComplexSigma], [FirstLitDelta,[],FirstComplexDelta]],JavaLeft), costruisciJava(RightProof,[[SecLitSigma,[],SecComplexSigma], [SecLitDelta,[],SecComplexDelta]],JavaRight). /* CEM */ costruisciJava(tree(cem,LeftProof,RightProof,U,Z,[X,A,Y]), [[LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta]], new_Tree(Sequente,cem,[[[X,A,Y]],[]],[[],[[X,A,Z]]],[[[X,A,U]],[]],JavaLeft,JavaRight)):- appiattisci([LitSigma,TransSigma,ComplexSigma],Antecedente), appiattisci([LitDelta,TransDelta,ComplexDelta],Conseguente), append(Antecedente,[*],Temp), append(Temp,Conseguente,Sequente), member([X,A,Y],TransSigma), costruisciJava(LeftProof,[[LitSigma,TransSigma,ComplexSigma], [LitDelta,[[X,A,Z]|TransDelta],ComplexDelta]],JavaLeft), labelSubstitution(LitSigma,Z,U,TempLitSigma), labelSubstitution(TempLitSigma,Y,U,DefLitSigma), labelSubstitution(TransSigma,Z,U,TempTransSigma), labelSubstitution(TempTransSigma,Y,U,DefTransSigma), labelSubstitution(ComplexSigma,Z,U,TempComplexSigma), labelSubstitution(TempComplexSigma,Y,U,DefComplexSigma), labelSubstitution(LitDelta,Z,U,TempLitDelta), labelSubstitution(TempLitDelta,Y,U,DefLitDelta), labelSubstitution(TransDelta,Z,U,TempTransDelta), labelSubstitution(TempTransDelta,Y,U,DefTransDelta), labelSubstitution(ComplexDelta,Z,U,TempComplexDelta), labelSubstitution(TempComplexDelta,Y,U,DefComplexDelta), costruisciJava(RightProof,[[DefLitSigma,DefTransSigma,DefComplexSigma], [DefLitDelta,DefTransDelta,DefComplexDelta]],JavaRight). /* ID */ costruisciJava(tree(id,LeftProof,[X,A,Y]), [[LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta]], new_Tree(Sequente,id,[[[X,A,Y]],[]],[[[Y,A]],[]],[[],[]],JavaLeft,null)):- appiattisci([LitSigma,TransSigma,ComplexSigma],Antecedente), appiattisci([LitDelta,TransDelta,ComplexDelta],Conseguente), append(Antecedente,[*],Temp), append(Temp,Conseguente,Sequente), put([Y,A],LitSigma,ComplexSigma,NewLitSigma,NewComplexSigma), costruisciJava(LeftProof,[[NewLitSigma,TransSigma,NewComplexSigma], [LitDelta,TransDelta,ComplexDelta]],JavaLeft). /* CS */ costruisciJava(tree(cs,LeftProof,RightProof,U,[X,A,Y]), [[LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta]], new_Tree(Sequente,cs,[[[X,A,Y]],[]],[[],[[X,A]]],[[[U,A,U]],[]],JavaLeft,JavaRight)):- appiattisci([LitSigma,TransSigma,ComplexSigma],Antecedente), appiattisci([LitDelta,TransDelta,ComplexDelta],Conseguente), append(Antecedente,[*],Temp), append(Temp,Conseguente,Sequente), member([X,A,Y],TransSigma), put([X,A],LitDelta,ComplexDelta,NewLitDelta,NewComplexDelta), costruisciJava(LeftProof,[[LitSigma,TransSigma,ComplexSigma], [NewLitDelta,TransDelta,NewComplexDelta]],JavaLeft), labelSubstitution(LitSigma,X,U,TempLitSigma), labelSubstitution(TempLitSigma,Y,U,DefLitSigma), labelSubstitution(TransSigma,X,U,TempTransSigma), labelSubstitution(TempTransSigma,Y,U,DefTransSigma), labelSubstitution(ComplexSigma,X,U,TempComplexSigma), labelSubstitution(TempComplexSigma,Y,U,DefComplexSigma), labelSubstitution(LitDelta,X,U,TempLitDelta), labelSubstitution(TempLitDelta,Y,U,DefLitDelta), labelSubstitution(TransDelta,X,U,TempTransDelta), labelSubstitution(TempTransDelta,Y,U,DefTransDelta), labelSubstitution(ComplexDelta,X,U,TempComplexDelta), labelSubstitution(TempComplexDelta,Y,U,DefComplexDelta), costruisciJava(RightProof,[[DefLitSigma,DefTransSigma,DefComplexSigma], [DefLitDelta,DefTransDelta,DefComplexDelta]],JavaRight).